Nuprl Definition : ma-init-val 11,40

M.init(x)?v == (M.2.2).1(x)?v 
latex



clarification:

M.init(x)?v == fpf-cap((M.2.2).1;IdDeq;x;v
latex


Definitionsf(x)?z, t.1, t.2, IdDeq
FDL editor aliasesma-init-val

origin